Lambda the Ultimate

Here is a diagram showing all the main programming paradigms and their relationships. This is quite different from the usual diagram which just shows programming languages. This diagram condenses a lot of information in a compact way. If your favorite language is not mentioned here, make a convincing argument and I may add it. If you find any errors, please let me know. I will take all people's comments into account to improve the diagram. Note to Unix aficionados: the diagram was made using xfig running on Mac OS X.

Edit: here is the latest updated diagram.

User level transactional programming in Haskell, Peter Thiemann, 2006 Haskell Workshop.

Correct handling of concurrently accessed external resources is a demanding problem in programming. The standard approaches rely on database transactions or concurrency mechanisms like locks. The paper considers two such resources, global variables and databases, and defines transactional APIs for them in Haskell. The APIs provide a novel flavor of user-level transactions which are particularly suitable in the context of web-based systems. This suitability is demonstrated by providing a second implementation in the context of WASH, a Haskell-based Web programming system. The underlying implementation framework works for both kinds of resources and can serve as a blueprint for further implementations of user-level transactions. The Haskell type system provides an encapsulation of the transactional scope that avoids unintended breakage of the transactional guarantees.

I thought this was an interesting paper because it gives a concrete example of a case where you want transactions, but positively don't want the full suite of ACID properties. Maybe it's not so surprising to those hardcore software architects in our audience who go to sleep with Jim Gray and Andreas Reuter's book under their pillows, though. :)

Compiling with Continuations, Continued, Andrew Kennedy. ICFP 2007.

We present a series of CPS-based intermediate languages suitable for functional language compilation, arguing that they have practical benefits over direct-style languages based on A-normal form (ANF) or monads. Inlining of functions demonstrates the benefits most clearly: in ANF-based languages, inlining involves a renormalization step that rearranges let expressions and possibly introduces a new ‘join point’ function, and in monadic languages, commuting conversions must be applied; in contrast, inlining in our CPS language is a simple substitution of variables for variables.

We present a contification transformation implemented by simple rewrites on the intermediate language. Exceptions are modelled using so-called ‘double-barrelled’ CPS. Subtyping on exception constructors then gives a very straightforward effect analysis for exceptions. We also show how a graph-based representation of CPS terms can be implemented extremely efficiently, with linear-time term simplification.

Analyzing the Environment Structure of Higher-Order Languages using Frame Strings, Matthew Might and Olin Shivers. 2007.

Reasoning about program behaviour in programming languages based on the lambda-calculus requires reasoning in a unified way about control, data and environment structure. Previous analysis work has done an inadequate job on the environment component of this task. We develop a new analytic framework, Delta-CFA, which is based on a new abstraction: frame strings, an enriched variant of procedure strings that can be used to model both control flow and environment allocation. This abstraction enables new environment-sensitive analyses and transformations that have not been previously attainable. We state the critical theorems needed to establish correctness of the entire technology suite, with their proofs.

Even if you're not interested in flow analysis of functional languages, the preface to this paper is very enjoyable reading. (If you are interested in flow analysis, the whole thing is enjoyable reading. I want a couple of weeks to go through this paper in detail.)

Validity Invariants and Effects, Yi Lu, John Potter and Jingling Xue. ECOOP 2007.

Object invariants describe the consistency of object states, and are crucial for reasoning about the correctness of object-oriented programs. However, reasoning about object invariants in the presence of object abstraction and encapsulation, arbitrary object aliasing and re-entrant method calls, is difficult. We present a general framework for reasoning about object invariants based on a behavioural abstraction that specifies two sets---the validity invariant, representing objects that must be valid before and after the behaviour, and the validity effect, describing objects that may be invalidated during the behaviour. The overlap of these two sets is critical because it captures precisely those objects that need to be re-validated at the end of the behaviour. When there is no overlap, no further validity checking is required. We also present a type system based on this framework. This system uses ownership types to confine dependencies for object invariants, and restricts permissible updates to track where object invariants hold even in the presence of re-entrant calls, but otherwise object referenceability and read access are not restricted.

I really liked this paper, but I think it might need a few preliminary explanations. There's a style of verification of OO programs based on "object invariants", which is the idea that you ensure that each object has an invariant, which every method maintains. Then verification is local, in the sense that you can verify each class's invariants independently. (This is used in the Boogie methodology used by Spec#, for instance.)

However, there are a couple of wrinkles. First, aliasing: every object's invariant depends on some of the objects in its fields, and you don't want random aliases letting strangers modify your representation objects underneath your feet. So you introduce a notion of ownership to help track who has permission to mess with each object. Second, reentrancy: suppose the middle of a method body has temporarily broken the object's invariant, and you call another method on the object? You don't a priori know the call is safe.

The type system the authors have introduced here tracks ownership and possibly-dangerous reentrant calls. The really clever part is that instead of just rejecting programs that fail these checks, they log all of the places where things break. So instead of saying "yes" or "no", the type system says "yes" or "manually verify the following things". So it's a labor-saving device for a verification methodology.

Morphing: Safely Shaping a Class in the Image of Others, Shan Shan Huang, David Zook, and Yannis Smaragdakis. ECOOP 2007.

We present MJ: a language for specifying general classes whose members are produced by iterating over members of other classes. We call this technique “class morphing” or just “morphing”. Morphing extends the notion of genericity so that not only types of methods and fields, but also the structure of a class can vary according to type variables. This offers the ability to express common programming patterns in a highly generic way that is otherwise not supported by conventional techniques. For instance, morphing lets us write generic proxies (i.e., classes that can be parameterized with another class and export the same public methods as that class); default implementations (e.g., a generic do-nothing type, configurable for any interface); semantic extensions (e.g., specialized behavior for methods that declare a certain annotation); and more. MJ’s hallmark feature is that, despite its emphasis on generality, it allows modular type checking: an MJ class can be checked independently of its uses. Thus, the possibility of supplying a type parameter that will lead to invalid code is detected early—an invaluable feature for highly general components that will be statically instantiated by other programmers.

This is related to the paper by Turon and Reppy I linked to yesterday; it's another take on compile-time metaprogramming. This time they have a static iteration over the structure of a class, which makes their safety result rather impressive. I talked Huang, and she told me that their big-picture goal is to eventually build a full language for manipulating programs at compile time, while still preserving all the safety guarantees we expect.

Expression and Loop Libraries for High-Performance Code Synthesis. Christopher Mueller and Andrew Lumsdaine. LCPC2006.

To simultaneously provide rapid application development and high performance, developers of scientific and multimedia applications often mix languages, using scripting languages to glue together high-performance components written in compiled languages. While this can be a useful development strategy, it distances application developers from the optimization process while adding complexity to the development tool chain. Recently, we introduced the Synthetic Programming Environment (SPE) for Python, a library for generating and executing machine instructions at run-time.

The authors didn't show much interest yet in supporting the most widespread ISAs, those for Intel processors. Instead they focus on PowerPC but also Cell. Have fun with Python and PS3 hacking.

Edit: You might also checkout the site of Christopher Mueller containing related material.

Joining this event (August 22-25) or following the action from afar may be a good way to keep up with Python 3000.

The first alpha release (3.0a1) should be just around the corner.

Metaprogramming with Traits, Aaron Turon and John Reppy. ECOOP 2007

In many domains, classes have highly regular internal structure. For example, so-called business objects often contain boilerplate code for mapping database fields to class members. The boilerplate code must be repeated per-field for every class, because existing mechanisms for constructing classes do not provide a way to capture and reuse such member-level structure. As a result, programmers often resort to ad ho code generation. This paper presents a lightweight mechanism for specifying and reusing member-level structure in Java programs. The proposal is based on a modest extension to traits that we have termed trait-based metaprogramming. Although the semantics of the mechanism are straightforward, its type theory is difficult to reconcile with nominal subtyping. We achieve reconciliation by introducing a hybrid structural/nominal type system that extends Java's type system. The paper includes a formal calculus defined by translation to Featherweight Generic Java.

This paper explains how to scratch an itch I've had for a long, long time -- uniformly generating groups of fields and methods, including computation of the field/method names. Something like this would be quite useful in an ML-like language's module system, too.

Generational Real-time Garbage Collection: A Three-part Invention for Young Objects, Daniel Frampton, David F. Bacon, Perry Cheng, David Grove. ECOOP 2007.

While real-time garbage collection is now available in production virtual machines, the lack of generational capability means applications with high allocation rates are subject to reduced throughput and high space overheads.

Since frequent allocation is often correlated with a high-level, object-oriented style of programming, this can force builders of real-time systems to compromise on software engineering.

We have developed a fully incremental, real-time generational collector based on a tri-partite nursery, which partitions the nursery into regions that are being allocated, collected, and promoted. Nursery collections are incremental, and can occur within any phase of a mature collection.

We present the design, mathematical model, and implementation of our collector in IBM's production Real-time Java virtual machine, and show both analytically and experimentally that the collector achieves real-time bounds comparable to a non-generational Metronome-style collector, while cutting memory consumption and total execution times by as much as 44% and 24% respectively.

Since the last post on GC was so popular, I figured I should post another one. The next few days I'll probably post links to a subset of the papers presented at ECOOP that a) I saw the talk for, and b) I found particularly striking from a language design POV.